#if !defined(PredicatesHeader)
#define PredicatesHeader

#include "node.h"

class Prototype;
class Prover;

class ProverFactoryBase {
public:
  virtual ~ProverFactoryBase () {
  }
  virtual Prover *instantiate () = 0;

  Node::NodeType nodeType;
  int clauseLength;
};

template<class ProverType>
class ProverFactory : public ProverFactoryBase {
public:
  Prover *instantiate () {
    return new ProverType;
  }
};

// Cannot be included earlier. Recursive header problems.
#include "prover.h"

// Registrar is to put the specified prover factory in the lookup list.

template<class ProverType, Node::NodeType nodeTypeID, //
    int clauseLength = 0> // Zero means no limit on clause length
class ProverFactoryRegistrar {
public:
  ProverFactoryRegistrar ();
  ~ProverFactoryRegistrar ();

  // Variable-argument predicate use another map. Decide which map to use
  Prover::ProversMap **forMap ();

  Prototype prototype;
  pNode node; // Maintains reference count

  static ProverFactory<ProverType> factory;
  static ProverFactoryRegistrar<ProverType, nodeTypeID, clauseLength> registrar;
};

template<class ProverType, Node::NodeType nodeTypeID, int clauseLength>
ProverFactory<ProverType> ProverFactoryRegistrar<ProverType, nodeTypeID,
    clauseLength>::factory;

template<class FactoryType, Node::NodeType nodeTypeID, int clauseLength>
ProverFactoryRegistrar<FactoryType, nodeTypeID, clauseLength>
    ProverFactoryRegistrar<FactoryType, nodeTypeID, clauseLength>::registrar;

template<class ProverType, Node::NodeType nodeTypeID, int clauseLength>
ProverFactoryRegistrar<ProverType, nodeTypeID, clauseLength>:: //
ProverFactoryRegistrar () {
  factory.clauseLength = clauseLength;
  factory.nodeType = nodeTypeID;

  // Creates our sample prototype
  Atom *atom;
  if(nodeTypeID != Tree::ID)
    node = atom = Atom::create (ProverType::name ());

  switch(nodeTypeID) {
  case Atom::ID:
    prototype = Prototype (atom);
    break;
  case Tree::ID:
    prototype = Prototype ((char*) ProverType::name ());
    break;
  case Tuple::ID:
    prototype = Prototype (atom, clauseLength);
    break;
  default:
    prototype = Prototype ();
  }

  // There are two maps, either for fixed- or variable-length predicates.
  // Choose one.
  Prover::ProversMap **map = forMap ();
  if(!*map)
    *map = new Prover::ProversMap;

  (*map)->insert (Prover::ProversMap::value_type (prototype, &factory));
}

template<class ProverType, Node::NodeType nodeTypeID, int clauseLength>
ProverFactoryRegistrar<ProverType, nodeTypeID, clauseLength>:: //
~ProverFactoryRegistrar () {
  Prover::ProversMap *map = *forMap ();
  map->erase (prototype);
  if(map->empty ())
    delete map;
}

template<class ProverType, Node::NodeType nodeTypeID, int clauseLength>
Prover::ProversMap **ProverFactoryRegistrar<ProverType, nodeTypeID,
    clauseLength>::forMap () {
  return (prototype.type == Tuple::ID && prototype.u.length == 0) //
  ? &Prover::varArgsProversMap
      : &Prover::proversMap;
}

#endif
